DETERMINISTIC FINITE AUTOMATA USINGCOUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT
Annotation
Subject of Research. The paper studies minimum-sized deterministic finite automata inferring problem. A hybrid method is developed and implemented reducing the given problem to Boolean satisfiability (SAT) technique and at the same time applying a counterexample guided abstraction refinement approach. Method. It is proposed to use not all given behavior examples as training data but start with some subset of them and build a consistent automaton, using SAT- based automata inferring method. Then the built automaton is checked against the complete set of behavior examples. The examples not consistent with the automaton are counterexamples. Some subset of counterexamples is added to the current training data and the process is being repeated. Main Results. The proposed method is implemented as a part of deterministic finite automata inferring tool in Python language. Experimental comparison of the developed method and the SAT-based method without abstraction refinement is carried out. Practical Relevance. Experimental research has shown that the developed method is reasonable for application if the number of behavior examples is large enough, at least, two hundred times exceeds the number of the automaton states, and, therefore, the Boolean formula being created contains tens and hundreds of millions of clauses.
Keywords
Постоянный URL
Articles in current issue
- EXPERIMENTAL METHOD FOR DETERMINATION OF SHRINKAGE DIRECTION DURING HOLOGRAPHIC RECORDING IN BAYFOL HX PHOTOPOLYMER
- AERIAL MAPPING BASED ON ARRANGEMENT OF OPTICAL ELECTRON CAMERAS
- Koreshev S.N., Starovoitov S.O., Smorodinov D.S., Frolova M.A.QUALITY ASSESSMENT OF BINARY OBJECT IMAGES RECONSTRUCTED BY COMPUTER-GENERATED HOLOGRAMS
- NONDESTRUCTIVE TESTING OF BALTIC AMBER:OPTICAL ANALYSIS OF MACRO- AND MICROSTRUCTURE
- FIBER OPTIC MEASUREMENT SYSTEM FOR DETERMINATION OF EXTENDED OBJECT POSITION AND BENDS IN 3D SPACE
- RECOVERY OF DISCRETE SPECTRA RADIATED BY SUBSTANCE IN DEEP VACUUM USING INTEGRAL APPROXIMATION ALGORITHM
- Omorov R.O.ROBUSTNESS RESEARCH OF INTERVAL DYNAMIC SYSTEMS BY ALGEBRAIC METHOD
- RESEARCH OF VISUAL SIMULTANEOUS LOCALIZATION AND MAPPING-BASED NAVIGATION SYSTEM FOR MOBILE ROBOTS
- REVIEW OF METHODS FOR SIZE AND MORPHOLOGY DETERMINATION OF VESICLES IN NIOSOME DISPERSION
- INFORMATION REPRESENTATION METHODS IN SIMPLE SEMANTIC NETWORKS
- DETERMINISTIC FINITE AUTOMATA USINGCOUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT
- DISTILLATION OF NEURAL NETWORK MODELS FOR DETECTION AND DESCRIPTION OF IMAGE KEY POINTS
- SOFTWARE PORTABILITY BASED ON RETARGETABLE RUNTIME ENVIRONMENt
- REAL TIME DETECTION AND CLASSIFICATION OF TRAFFIC SIGNS BASED ON YOLO VERSION 3 ALGORITHM (in English)
- U-NET ARCHITECTURE NEURAL NETWORK FOR LOCALIZATION OF DIGITAL IMAGES INTEGRITY VIOLATION
- DETERMINISTIC SYSTEMS WITH NATURAL QUANTIZATION
- TECHNICAL PNEUMOSYSTEM FOR DEVELOPMENT OF DEVICES WITH CERTAIN FUNCTIONAL CAPABILITIES
- STATISTICAL MODELING OF KNEE JOINT GEAR RATIOS
- COMPARISON OF BEAMFORMING ALGORITHMS FOR MICROPHONE ARRAYS IN MATLAB
- QR CODES WITH ANIMATION FOR DIGITAL PASSES
- PHOTOACTINIC IRRADIATION EFFECT ON REFRACTION INDICE OF ORGANIC CO-CRYSTALS BASED ON AMINOPYRIDINE SERIES